ds,da,x,T:top, ks:(top List), tr:top, j,i:Id.
sqequal(R-has-loc(R-state-var(i; ds; da; x; T; ks; tr); j); eq_id(i; j)) 

latex

Definitions	Y, if b then t else f fi , prop{i:l}, tt, P  Q, ff, reduce(f; k; as), bor(p; q), x. t(x), t  T, R-state-var(i; ds; da; x; T; ks; tr), R-has-loc(R; i), top, x:A. B(x), guard(T), sq_type(T), P  Q, P  Q, Unit, , x(s),
Lemmas	bool sq, bfalse wf, not functionality wrt iff, assert of bnot, eqff to assert, not wf, bnot wf, btrue wf, assert-eq-id, eqtt to assert, assert wf, iff transitivity, bool wf, eq id wf, top wf, Id wf, Rall-has-loc